YES 5.673
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ IFR
mainModule List
| ((union :: [Char] -> [Char] -> [Char]) :: [Char] -> [Char] -> [Char]) |
module List where
| import qualified Maybe import qualified Prelude
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | _ _ [] | = | [] |
deleteBy | eq x (y : ys) | = | if x `eq` y then ys else y : deleteBy eq x ys |
|
| elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
elem_by | _ _ [] | = | False |
elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| nubBy :: (a -> a -> Bool) -> [a] -> [a]
nubBy | eq l | = |
nubBy' l [] | where |
nubBy' | [] _ | = | [] |
nubBy' | (y : ys) xs | |
| | elem_by eq y xs | = |
|
| | otherwise | = |
|
|
|
|
|
|
| union :: Eq a => [a] -> [a] -> [a]
|
| unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| import qualified List import qualified Prelude
|
If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys
is transformed to
deleteBy0 | ys y eq x True | = ys |
deleteBy0 | ys y eq x False | = y : deleteBy eq x ys |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
| ((union :: [Char] -> [Char] -> [Char]) :: [Char] -> [Char] -> [Char]) |
module List where
| import qualified Maybe import qualified Prelude
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | _ _ [] | = | [] |
deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
|
deleteBy0 | ys y eq x True | = | ys |
deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
elem_by | _ _ [] | = | False |
elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| nubBy :: (a -> a -> Bool) -> [a] -> [a]
nubBy | eq l | = |
nubBy' l [] | where |
nubBy' | [] _ | = | [] |
nubBy' | (y : ys) xs | |
| | elem_by eq y xs | = |
|
| | otherwise | = |
|
|
|
|
|
|
| union :: Eq a => [a] -> [a] -> [a]
|
| unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((union :: [Char] -> [Char] -> [Char]) :: [Char] -> [Char] -> [Char]) |
module List where
| import qualified Maybe import qualified Prelude
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | vw vx [] | = | [] |
deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
|
deleteBy0 | ys y eq x True | = | ys |
deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
elem_by | vz wu [] | = | False |
elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| nubBy :: (a -> a -> Bool) -> [a] -> [a]
nubBy | eq l | = |
nubBy' l [] | where |
nubBy' | [] vy | = | [] |
nubBy' | (y : ys) xs | |
| | elem_by eq y xs | = |
|
| | otherwise | = |
|
|
|
|
|
|
| union :: Eq a => [a] -> [a] -> [a]
|
| unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
nubBy' | [] vy | = [] |
nubBy' | (y : ys) xs |
| | elem_by eq y xs | |
| | otherwise | |
|
is transformed to
nubBy' | [] vy | = nubBy'3 [] vy |
nubBy' | (y : ys) xs | = nubBy'2 (y : ys) xs |
nubBy'1 | y ys xs True | = nubBy' ys xs |
nubBy'1 | y ys xs False | = nubBy'0 y ys xs otherwise |
nubBy'0 | y ys xs True | = y : nubBy' ys (y : xs) |
nubBy'2 | (y : ys) xs | = nubBy'1 y ys xs (elem_by eq y xs) |
nubBy'3 | [] vy | = [] |
nubBy'3 | wz xu | = nubBy'2 wz xu |
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule List
| ((union :: [Char] -> [Char] -> [Char]) :: [Char] -> [Char] -> [Char]) |
module List where
| import qualified Maybe import qualified Prelude
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | vw vx [] | = | [] |
deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
|
deleteBy0 | ys y eq x True | = | ys |
deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
elem_by | vz wu [] | = | False |
elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| nubBy :: (a -> a -> Bool) -> [a] -> [a]
nubBy | eq l | = |
nubBy' l [] | where |
nubBy' | [] vy | = | nubBy'3 [] vy |
nubBy' | (y : ys) xs | = | nubBy'2 (y : ys) xs |
|
nubBy'0 | y ys xs True | = | y : nubBy' ys (y : xs) |
|
nubBy'1 | y ys xs True | = | nubBy' ys xs |
nubBy'1 | y ys xs False | = | nubBy'0 y ys xs otherwise |
|
nubBy'2 | (y : ys) xs | = | nubBy'1 y ys xs (elem_by eq y xs) |
|
nubBy'3 | [] vy | = | [] |
nubBy'3 | wz xu | = | nubBy'2 wz xu |
|
|
|
|
| union :: Eq a => [a] -> [a] -> [a]
|
| unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| import qualified List import qualified Prelude
|
Let/Where Reductions:
The bindings of the following Let/Where expression
nubBy' l [] |
where |
nubBy' | [] vy | = nubBy'3 [] vy |
nubBy' | (y : ys) xs | = nubBy'2 (y : ys) xs |
|
|
nubBy'0 | y ys xs True | = y : nubBy' ys (y : xs) |
|
|
nubBy'1 | y ys xs True | = nubBy' ys xs |
nubBy'1 | y ys xs False | = nubBy'0 y ys xs otherwise |
|
|
nubBy'2 | (y : ys) xs | = nubBy'1 y ys xs (elem_by eq y xs) |
|
|
nubBy'3 | [] vy | = [] |
nubBy'3 | wz xu | = nubBy'2 wz xu |
|
are unpacked to the following functions on top level
nubByNubBy'2 | xv (y : ys) xs | = nubByNubBy'1 xv y ys xs (elem_by xv y xs) |
nubByNubBy'0 | xv y ys xs True | = y : nubByNubBy' xv ys (y : xs) |
nubByNubBy' | xv [] vy | = nubByNubBy'3 xv [] vy |
nubByNubBy' | xv (y : ys) xs | = nubByNubBy'2 xv (y : ys) xs |
nubByNubBy'1 | xv y ys xs True | = nubByNubBy' xv ys xs |
nubByNubBy'1 | xv y ys xs False | = nubByNubBy'0 xv y ys xs otherwise |
nubByNubBy'3 | xv [] vy | = [] |
nubByNubBy'3 | xv wz xu | = nubByNubBy'2 xv wz xu |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule List
| (union :: [Char] -> [Char] -> [Char]) |
module List where
| import qualified Maybe import qualified Prelude
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | vw vx [] | = | [] |
deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
|
deleteBy0 | ys y eq x True | = | ys |
deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
elem_by | vz wu [] | = | False |
elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| nubBy :: (a -> a -> Bool) -> [a] -> [a]
nubBy | eq l | = | nubByNubBy' eq l [] |
|
|
nubByNubBy' | xv [] vy | = | nubByNubBy'3 xv [] vy |
nubByNubBy' | xv (y : ys) xs | = | nubByNubBy'2 xv (y : ys) xs |
|
|
nubByNubBy'0 | xv y ys xs True | = | y : nubByNubBy' xv ys (y : xs) |
|
|
nubByNubBy'1 | xv y ys xs True | = | nubByNubBy' xv ys xs |
nubByNubBy'1 | xv y ys xs False | = | nubByNubBy'0 xv y ys xs otherwise |
|
|
nubByNubBy'2 | xv (y : ys) xs | = | nubByNubBy'1 xv y ys xs (elem_by xv y xs) |
|
|
nubByNubBy'3 | xv [] vy | = | [] |
nubByNubBy'3 | xv wz xu | = | nubByNubBy'2 xv wz xu |
|
| union :: Eq a => [a] -> [a] -> [a]
|
| unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xw1000), Succ(xw9000)) → new_primEqNat(xw1000, xw9000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xw1000), Succ(xw9000)) → new_primEqNat(xw1000, xw9000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_nubByNubBy'10(xw155, xw156, xw157, xw158, :(xw1600, xw1601)) → new_nubByNubBy'1(xw155, xw156, xw157, xw158, new_primEqChar(xw1600, xw155), xw1601)
new_nubByNubBy'1(xw155, xw156, xw157, xw158, False, :(xw1600, xw1601)) → new_nubByNubBy'1(xw155, xw156, xw157, xw158, new_primEqChar(xw1600, xw155), xw1601)
new_nubByNubBy'10(xw155, xw156, xw157, xw158, []) → new_nubByNubBy'(xw156, xw155, :(xw157, xw158))
new_nubByNubBy'1(xw155, xw156, xw157, xw158, False, []) → new_nubByNubBy'(xw156, xw155, :(xw157, xw158))
new_nubByNubBy'1(xw155, :(xw1560, xw1561), xw157, xw158, True, xw160) → new_nubByNubBy'10(xw1560, xw1561, xw157, xw158, :(xw157, xw158))
new_nubByNubBy'(:(xw1560, xw1561), xw157, xw158) → new_nubByNubBy'10(xw1560, xw1561, xw157, xw158, :(xw157, xw158))
The TRS R consists of the following rules:
new_primEqNat0(Succ(xw1000), Zero) → False
new_primEqNat0(Zero, Succ(xw9000)) → False
new_primEqChar(Char(xw100), Char(xw900)) → new_primEqNat0(xw100, xw900)
new_primEqNat0(Succ(xw1000), Succ(xw9000)) → new_primEqNat0(xw1000, xw9000)
new_primEqNat0(Zero, Zero) → True
The set Q consists of the following terms:
new_primEqChar(Char(x0), Char(x1))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Succ(x0), Succ(x1))
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_nubByNubBy'10(xw155, xw156, xw157, xw158, :(xw1600, xw1601)) → new_nubByNubBy'1(xw155, xw156, xw157, xw158, new_primEqChar(xw1600, xw155), xw1601)
new_nubByNubBy'1(xw155, xw156, xw157, xw158, False, :(xw1600, xw1601)) → new_nubByNubBy'1(xw155, xw156, xw157, xw158, new_primEqChar(xw1600, xw155), xw1601)
new_nubByNubBy'1(xw155, xw156, xw157, xw158, False, []) → new_nubByNubBy'(xw156, xw155, :(xw157, xw158))
new_nubByNubBy'1(xw155, :(xw1560, xw1561), xw157, xw158, True, xw160) → new_nubByNubBy'10(xw1560, xw1561, xw157, xw158, :(xw157, xw158))
new_nubByNubBy'(:(xw1560, xw1561), xw157, xw158) → new_nubByNubBy'10(xw1560, xw1561, xw157, xw158, :(xw157, xw158))
The TRS R consists of the following rules:
new_primEqNat0(Succ(xw1000), Zero) → False
new_primEqNat0(Zero, Succ(xw9000)) → False
new_primEqChar(Char(xw100), Char(xw900)) → new_primEqNat0(xw100, xw900)
new_primEqNat0(Succ(xw1000), Succ(xw9000)) → new_primEqNat0(xw1000, xw9000)
new_primEqNat0(Zero, Zero) → True
The set Q consists of the following terms:
new_primEqChar(Char(x0), Char(x1))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Succ(x0), Succ(x1))
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_nubByNubBy'1(xw155, xw156, xw157, xw158, False, :(xw1600, xw1601)) → new_nubByNubBy'1(xw155, xw156, xw157, xw158, new_primEqChar(xw1600, xw155), xw1601)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 > 6
- new_nubByNubBy'10(xw155, xw156, xw157, xw158, :(xw1600, xw1601)) → new_nubByNubBy'1(xw155, xw156, xw157, xw158, new_primEqChar(xw1600, xw155), xw1601)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 6
- new_nubByNubBy'(:(xw1560, xw1561), xw157, xw158) → new_nubByNubBy'10(xw1560, xw1561, xw157, xw158, :(xw157, xw158))
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3, 3 >= 4
- new_nubByNubBy'1(xw155, xw156, xw157, xw158, False, []) → new_nubByNubBy'(xw156, xw155, :(xw157, xw158))
The graph contains the following edges 2 >= 1, 1 >= 2
- new_nubByNubBy'1(xw155, :(xw1560, xw1561), xw157, xw158, True, xw160) → new_nubByNubBy'10(xw1560, xw1561, xw157, xw158, :(xw157, xw158))
The graph contains the following edges 2 > 1, 2 > 2, 3 >= 3, 4 >= 4
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy(xw10, :(xw90, xw91), bb) → new_deleteBy0(xw91, xw90, xw10, new_esEs(xw10, xw90, bb), bb)
new_deleteBy0(xw17, xw18, xw19, False, ba) → new_deleteBy(xw19, xw17, ba)
The TRS R consists of the following rules:
new_esEs(xw10, xw90, app(app(app(ty_@3, bg), bh), ca)) → error([])
new_esEs(xw10, xw90, ty_Double) → error([])
new_primEqNat0(Succ(xw1000), Zero) → False
new_primEqNat0(Zero, Succ(xw9000)) → False
new_esEs(xw10, xw90, ty_Integer) → error([])
new_primEqChar(Char(xw100), Char(xw900)) → new_primEqNat0(xw100, xw900)
new_esEs(xw10, xw90, ty_Ordering) → error([])
new_esEs(xw10, xw90, app(app(ty_@2, be), bf)) → error([])
new_esEs(xw10, xw90, app(ty_[], bd)) → error([])
new_esEs(xw10, xw90, app(ty_Ratio, cd)) → error([])
new_esEs(xw10, xw90, ty_@0) → error([])
new_esEs(xw10, xw90, ty_Bool) → error([])
new_primEqNat0(Succ(xw1000), Succ(xw9000)) → new_primEqNat0(xw1000, xw9000)
new_primEqNat0(Zero, Zero) → True
new_esEs(xw10, xw90, ty_Char) → new_primEqChar(xw10, xw90)
new_esEs(xw10, xw90, app(app(ty_Either, cb), cc)) → error([])
new_esEs(xw10, xw90, ty_Float) → error([])
new_esEs(xw10, xw90, app(ty_Maybe, bc)) → error([])
new_esEs(xw10, xw90, ty_Int) → error([])
The set Q consists of the following terms:
new_esEs(x0, x1, ty_Double)
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_esEs(x0, x1, ty_@0)
new_primEqNat0(Zero, Zero)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs(x0, x1, ty_Ordering)
new_esEs(x0, x1, ty_Int)
new_primEqNat0(Zero, Succ(x0))
new_esEs(x0, x1, ty_Integer)
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs(x0, x1, ty_Char)
new_primEqChar(Char(x0), Char(x1))
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, ty_Bool)
new_esEs(x0, x1, app(ty_Ratio, x2))
new_esEs(x0, x1, ty_Float)
new_esEs(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Succ(x0), Zero)
new_esEs(x0, x1, app(ty_[], x2))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy0(xw17, xw18, xw19, False, ba) → new_deleteBy(xw19, xw17, ba)
The graph contains the following edges 3 >= 1, 1 >= 2, 5 >= 3
- new_deleteBy(xw10, :(xw90, xw91), bb) → new_deleteBy0(xw91, xw90, xw10, new_esEs(xw10, xw90, bb), bb)
The graph contains the following edges 2 > 1, 2 > 2, 1 >= 3, 3 >= 5
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldl(xw9, xw10, :(xw110, xw111), ba) → new_foldl(new_flip(xw9, xw10, ba), xw110, xw111, ba)
The TRS R consists of the following rules:
new_primEqChar(Char(xw100), Char(xw900)) → new_primEqNat0(xw100, xw900)
new_esEs(xw10, xw90, ty_Ordering) → error([])
new_esEs(xw10, xw90, ty_@0) → error([])
new_esEs(xw10, xw90, app(ty_Ratio, cc)) → error([])
new_deleteBy00(xw17, xw18, xw19, True, cd) → xw17
new_esEs(xw10, xw90, ty_Bool) → error([])
new_primEqNat0(Succ(xw1000), Succ(xw9000)) → new_primEqNat0(xw1000, xw9000)
new_primEqNat0(Zero, Zero) → True
new_esEs(xw10, xw90, ty_Char) → new_primEqChar(xw10, xw90)
new_esEs(xw10, xw90, app(app(ty_Either, ca), cb)) → error([])
new_deleteBy1(xw10, [], ba) → []
new_esEs(xw10, xw90, app(app(app(ty_@3, bf), bg), bh)) → error([])
new_esEs(xw10, xw90, ty_Double) → error([])
new_primEqNat0(Succ(xw1000), Zero) → False
new_primEqNat0(Zero, Succ(xw9000)) → False
new_esEs(xw10, xw90, ty_Integer) → error([])
new_esEs(xw10, xw90, app(app(ty_@2, bd), be)) → error([])
new_esEs(xw10, xw90, app(ty_[], bc)) → error([])
new_deleteBy00(xw17, xw18, xw19, False, cd) → :(xw18, new_deleteBy1(xw19, xw17, cd))
new_deleteBy1(xw10, :(xw90, xw91), ba) → new_deleteBy00(xw91, xw90, xw10, new_esEs(xw10, xw90, ba), ba)
new_flip(xw9, xw10, ba) → new_deleteBy1(xw10, xw9, ba)
new_esEs(xw10, xw90, ty_Float) → error([])
new_esEs(xw10, xw90, app(ty_Maybe, bb)) → error([])
new_esEs(xw10, xw90, ty_Int) → error([])
The set Q consists of the following terms:
new_esEs(x0, x1, ty_Double)
new_deleteBy00(x0, x1, x2, True, x3)
new_esEs(x0, x1, ty_@0)
new_deleteBy1(x0, [], x1)
new_primEqNat0(Zero, Zero)
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs(x0, x1, ty_Ordering)
new_deleteBy1(x0, :(x1, x2), x3)
new_esEs(x0, x1, app(ty_[], x2))
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, ty_Int)
new_flip(x0, x1, x2)
new_primEqNat0(Zero, Succ(x0))
new_esEs(x0, x1, ty_Integer)
new_esEs(x0, x1, app(ty_Ratio, x2))
new_esEs(x0, x1, app(ty_Maybe, x2))
new_esEs(x0, x1, ty_Char)
new_primEqChar(Char(x0), Char(x1))
new_esEs(x0, x1, ty_Bool)
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_esEs(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Zero)
new_deleteBy00(x0, x1, x2, False, x3)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldl(xw9, xw10, :(xw110, xw111), ba) → new_foldl(new_flip(xw9, xw10, ba), xw110, xw111, ba)
The graph contains the following edges 3 > 2, 3 > 3, 4 >= 4
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs(:(xw80, xw81), xw9, xw10, xw11, ba) → new_psPs(xw81, xw9, xw10, xw11, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(:(xw80, xw81), xw9, xw10, xw11, ba) → new_psPs(xw81, xw9, xw10, xw11, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5